DerivingVia sums-of-products

I like the generics-sop way of modeling generic types as a promoted list of list of types: [[Type]]. "Sums of products" represents Bool with two constructors (sums) generically as a list of length two. The inner lists represent the arguments of the constructors (products).

Since False and True take no arguments the inner lists of Code Bool = '[ '[], '[] ] are empty.

> import Generics.SOP
>
> :kind! Code Bool
Code Bool :: [[*]]
= '[ '[], '[]]
> :kind! Code (Maybe Int)
Code (Maybe Int) :: [[*]]
= '[ '[], '[Int]]
> :kind! Code (Either Int Bool)
Code (Either Int Bool) :: [[*]]
= '[ '[Int], '[Bool]]
> :kind! Code ((), (), (), (), ())
Code ((), (), (), (), ()) :: [[*]]
= '[ '[(), (), (), (), ()]]

GenericallySOP

It is easy to define a GenericallySOP modifier for generic Semigroup and Monoid instances. I adapted code from here but it's not important to understand the details.

type    GenercallySOP :: Type -> Type
newtype GenercallySOP a = GenercallySOP a

instance
  ( SOP.Generic a
  , IsProductType a as
  , SOP.All Semigroup as
  ) => Semigroup (GenercallySOP a) where
 (<>) :: GenercallySOP a -> GenercallySOP a -> GenercallySOP a
 (<>) = coerce m where

    m :: a -> a -> a
    m (from -> SOP (Z as)) (from -> SOP (Z bs)) = 
      to $ SOP $ Z $ hcliftA2 @_ @Semigroup Proxy (liftA2 (<>)) as bs

instance
  ( SOP.Generic a
  , IsProductType a as
  , SOP.All Semigroup as
  , SOP.All Monoid as
  )
    =>
  Monoid (GenercallySOP a) where
  mempty :: GenercallySOP a
  mempty = GenercallySOP $ to $ SOP $ Z $ hcpure @_ @_ @_ @Monoid Proxy (I mempty)

This allows us to derive monoid instances assuming that each field of the datatype is a monoid.

type Strs :: Type
data Strs = Strs String String
  deriving
    ( Semigroup   -- Strs a b <> Strs a' b' = Strs (a++a') (b++b')
    , Monoid      -- mempty                 = Strs "" ""
    )
  via GenericallySOP Strs

ah assuming we have derived its SOP.Generic instance which relies on the GHC.Generic instance

  deriving
  stock GHC.Generic
  
  deriving
  anyclass SOP.Generic

What if some of the fields aren't monoids? What if they are monoids in more ways than one?

Core Idea

Core idea: given two codes code, code' we can safely (unsafe)Coerce their generic representations SOP I code, SOP I code' if the element are coercible (pointwise) (AllZip2 Coercible code code'). Coercible means being represented the same at runtime.This has numerous applications. It's not uncommon to see a datatype that is essentially a product of monoids with non-default behaviour.

Int is an example of a type that has no semigroup instance, yet addition and multiplication form a semigroup.
[Bool] is a monoid but in more ways than one. As you see we use something more exotic than the normal ++ and [] behaviour of lists.

This also can be derived.

--
-- Code (Foo a) = '[ '[ Int, Int, [Bool], a->a ] ]
--
type Foo :: Type -> Type
data Foo a = Foo
  { one   :: Int
  , two   :: Int
  , three :: [Bool]
  , four  :: a->a
  }

instance Semigroup (Foo a) where
  (<>) :: Foo a -> Foo a -> Foo a
  Foo a b cs d <> Foo a' b' cs' d' =
    Foo (a + a') (b * b') (zipWith (&&) cs cs') (d . d')

instance Monoid (Foo a) where
  mempty :: Foo a
  mempty = Foo 0 1 (repeat True) id

Attempt 1: `newtype`

For a long time we have had generalized newtype deriving which allows deriving via the underlying representation of a datatype. This uses the fact that pairs are monoids if each component is:

instance (Semigroup a, Semigroup b) => Semigroup (a, b)
instance    (Monoid a,    Monoid b) =>    Monoid (a, b)

Sum Int indicates + and 0
Product Int indicates * and 1
Ap ZipList All indicate zipWith (&&) and repeat True
All indicates && and True
Endo a indicates . and id

These modifiers give their underlying types different behaviour but they add unsightly noise to the actual constructor:

type    Foo :: Type -> Type
newtype Foo a = Foo 
  (Sum Int, Product Int, Ap ZipList All, Endo a)
  deriving
  newtype (Semigroup, Monoid)

Attempt 2: `via`

Such low-level details shouldn't matter when using Foo. Deriving via solves that by factoring it out into a via type but leaves a different problem.

type    Foo :: Type -> Type
newtype Foo a = Foo (Int, Int, [Bool], a->a)
  deriving
    (Semigroup, Monoid) 
  via
    (Sum Int, Product Int, Ap ZipList All, Endo a)

Final attempt: pretending `via`

We want Foo to be curried and to use record syntax. We could reach for pattern synonyms over a newtype but in this case it does not encourage a natural style of writing. We don't want deriving to change our datatype.

type Foo :: Type -> Type
data Foo a = Foo
  { one   :: Int
  , two   :: Int
  , three :: [Bool]
  , four  :: a->a
  }
  deriving
    (Semigroup, Monoid)
  via
    GenericallySOP
      (Foo a
        `PretendingVia`
      '[ '[ Sum Int, Product Int, Ap ZipList All, Endo a ] ])

and mandatory deriving generics:

  deriving stock    GHC.Generic
  deriving anyclass SOP.Generic

This is the heart of this article. PretendingVia hijacks a SOP.Generic instance and injects a custom "via code".

type    PretendingVia :: Type -> [[Type]] -> Type
newtype a `PretendingVia` viacode = PretendingVia
  { pretendVia :: a
  }

This is based on a single assumption that it is indeed safe to coerce between Rep a = SOP I (Code a) and SOP I viacode:

instance
  ( SOP.All SListI viacode
  , Generic a
  , AllZip2 Coercible viacode (Code a)
  , AllZip2 Coercible (Code a) viacode
  )
    =>
  Generic (PretendingVia a viacode) where
  type Code (PretendingVia a viacode) = viacode

  to :: SOP I viacode -> PretendingVia a viacode
  to = axiom @viacode @(Code a) >>> to >>> PretendingVia

  from :: PretendingVia a viacode -> SOP I viacode
  from = pretendVia >>> from >>> axiom @(Code a) @viacode

expressed as this axiom

axiom :: forall code0 code1. 
         AllZip2 Coercible code0 code1
      => SOP I code0
      -> SOP I code1
axiom = unsafeCoerce

Higher-Order Abstract Syntax

Attempting to stock derive Ord Exp or Show Exp is not possible because Exp->Exp has none of those instances.

--
-- Code Exp = '[ '[Exp, Exp], '[Exp->Exp] ]
--
type Exp :: Type
data Exp = App Exp Exp | Lam (Exp -> Exp)

Since Exp->Exp is coercible to Hidden (Exp->Exp) we can view '[ '[Exp, Exp], '[Hidden (Exp->Exp)] ] as the Exp code which ignores the function argument.

type    Hidden :: Type -> Type
newtype Hidden a = Hidden a

instance Show (Hidden a) where
 show :: Hidden a -> String
 show _ = "(*)"

instance Eq (Hidden a) where
 (==) :: Hidden a -> Hidden a -> Bool
 _ == _ = True

instance Ord (Hidden a) where
 compare :: Hidden a -> Hidden a -> Ordering
 compare _ _ = EQ

As before we require an instance of GenericallySOP this time taken directly from Generics.SOP.Eq:

instance (Generic a , All2 Eq (Code a)) => Eq (GenercallySOP a) where
 (==) :: GenercallySOP a -> GenercallySOP a -> Bool
 (==) = coerce (geq @a)

This

type Exp :: Type
data Exp = App Exp Exp | Lam (Exp -> Exp)

  deriving
    Eq
  via
   GenercallySOP
     (Exp
         `PretendingVia`
     '[ '[ Exp, Exp ]
      , '[ Hidden (Exp->Exp) ]
      ])

with

  deriving stock    GHC.Generic
  deriving anyclass SOP.Generic

means you can compare Lam id == Lam (\f -> App f f) for equality. And it gives back True. Well it's possible anyway, and relatively little fuss.

Links